\label{sec:verifyingVerification}

\begin{definition}{Transformation Instance Symbolic Map}
\label{def:transf_instance_siblings}

Define this at the level of the match-apply graphs. Resulting match apply-graphs
from transformations and final states from the symbolic executions. Do the
backward links need to be part of the homomorphism for the mapping? 
\end{definition}

\begin{definition}{Transformation Instance Siblings}
\label{def:transf_instance_siblings}

Let $tf\in Transformation^{s}_{t}$ be a model transformation and
$\{ti,ti'\}\subseteq TRStep_{tr}$ be \emph{transformation instances}. $ti$ and
$ti'$ are transformation instances siblings, noted $ti\sim ti'$, iff there
exists a symbolic execution $se\in SE_{tr}$ such that $ti\Vvdash se$ and
$ti'\Vvdash se$.
\end{definition}

\begin{lemma}{Symbolic Execution Uniqueness}

Let $tr\in Transformation^{s}_{t}$ be a model transformation, $ti\in
TRStep_{tr}$ be a \emph{transformation instance} and $\{se,se'\}\subseteq SE_{tr}$ be a
\emph{symbolic execution}. If $ti\Vvdash se$ and $ti\Vvdash se'$ then $se=se'$.
\end{lemma}
\begin{proof}
\end{proof}

\begin{proposition}{The sibling relation $\sim$ is an equivalence relation.}
\end{proposition}
\begin{proof}
In order to prove that $\sim$ is an equivalence relation we have to prove that
$\sim$ is \emph{reflexive}, \emph{transitive} and \emph{symmetric}. In the
following assume $tf\in Transformation^{s}_{t}$, $\{ti,ti',ti''\}\subseteq
TRStep_{tf}$ \emph{transformation instances} and $ti\sim ti'$.

In order to prove that $\sim$ is \emph{reflexive} let us assume that $ti\Vvdash
se$, where $se\in SE_{tf}$. Then, using the definition of transformation
instances siblings, $ti\Vvdash se\;\land\;ti\Vvdash se$ is a true formula. Thus
$ti\sim ti$.

In order to prove that $\sim$ is \emph{symmetric} let us assume that $ti\sim
ti'$. Then there exists a symbolic execution $se\in SE_{tf}$ such that
$ti\Vvdash se \land ti'\Vvdash se$. Because of the commutativity of $\land$
$ti'\Vvdash se \land ti\Vvdash se$ and thus $ti'\sim ti$.

In order to prove that $\sim$ is \emph{transitive} let us assume that $ti\sim
ti'$ and $ti'\sim ti''$. Then there exists $\{se,se'\}\subseteq SE_{tf}$ such
that $ti\Vvdash se\;\land\;ti'\Vvdash se$ and $ti'\Vvdash se'\;\land\;ti''\Vvdash
se'$. In order for $\sim$ to be \emph{transitive} then $ti\sim ti''$ has to
hold. This happens if $se=se'$.
\end{proof}

\begin{theorem}{Completeness}

Let $tf\in Transformation^{s}_{t}$ be a transformation. For all
transformation instance $ti\in TRStep_{tf}$ there exists one and only one
symbolic execution $se\in SE_{tf}$ such that $ti\Vvdash se$.
\end{theorem}
\begin{proof}
We will prove the property by induction on the number of layers in a
transformation. We will firstly establish the base case which happens when $tf=[l]$ includes
only one layer where $l\in Layer^{s}_{t}$. We will then go on to show that
assuming the hypothesis holds for a transformation with a number of layers
$k$, it will hold for a transformation with a number of layers $k+1$.\\

Let $l\in Layer^{s}_{t}$. In order to prove the base case we will show by
induction on the size of a layer that for all transformation instance $ti\in
TRStep_[l]$ there exists one and only one symbolic execution $se\in SE_[l]$ such that
$ti\Vvdash se$.

\begin{itemize}
  \item Base case: Layer $l=\{tr\}$ includes only one transformation rule where
  $t=\langle V,E,\tau,Match,Apply,Bl,Il\rangle\in TR^{s}_{t}$.\\

In this case $SE_{[l]}$ is formed by the powerset $\mathcal{P}(l)$
(definition~\ref{def:layer_combinations}). By applying the first axiom in
definition~\ref{def:transf_state_space} the set of symbolic executions built is
$SE_{[l]}=\{\emptyset,tr\}$. $TRStep_{[l]}$ is built by matching the $Match$
subgraph upon models $\langle V',E',\tau',s\rangle\in MODEL^s$. We have to
analyse two cases:\\

\begin{itemize}
\item $match_{tr}(m)=\emptyset$ -- in this case $apply_{tr}(m)=\emptyset$ and by
invoking the axiom 2 of definition~\ref{def:transformation_step_semantics} the
axiom 2 of definition~\ref{def:layer_step_semantics} is invoked thus building 
\end{itemize}\\

Fazer a demonstracao para o caso onde nao ha matches e por inducao para o caso
onde ha mais de um match. Propriedade: se a producao de uma uniao de matches e
instancia de uma execucao simbolica, entao a uniao com mais um match continua a
ser instancia da mesma execucao simbolica.\\

\item Induction step: Layer $l$ includes several transformation rules. If the
property holds for layer $l$ then it holds for layer $l\cup \{tr\}$ where
$tr\in TR^{s}_{t}$.\\
\end{itemize}

We now need to prove the induction step for main theorem. We need to show that
if the property holds for a transformation $tf\in Transformation^{s}_{t}$, it
will hold for a transformation $[l::tf]$, where $[l::tf]$ is transformation $tf$
incremented by layer $l$.

\end{proof}

\begin{theorem}{Validity}

Let $tf\in Transformation^{s}_{t}$ be a transformation. For all symbolic execution
$se\in SE_{tf}$ there exists a transformation instance $ti\in TRStep_{tf}$ such
that $ti\Vvdash se$.
\end{theorem}
\begin{proof}
\end{proof}